'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ double(0()) -> 0()
, double(s(x)) -> s(s(double(x)))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y)
, if(0(), y, z) -> y
, if(s(x), y, z) -> z
, half(double(x)) -> x}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ double^#(0()) -> c_0()
, double^#(s(x)) -> c_1(double^#(x))
, half^#(0()) -> c_2()
, half^#(s(0())) -> c_3()
, half^#(s(s(x))) -> c_4(half^#(x))
, -^#(x, 0()) -> c_5()
, -^#(s(x), s(y)) -> c_6(-^#(x, y))
, if^#(0(), y, z) -> c_7()
, if^#(s(x), y, z) -> c_8()
, half^#(double(x)) -> c_9()}
The usable rules are:
{}
The estimated dependency graph contains the following edges:
{double^#(s(x)) -> c_1(double^#(x))}
==> {double^#(s(x)) -> c_1(double^#(x))}
{double^#(s(x)) -> c_1(double^#(x))}
==> {double^#(0()) -> c_0()}
{half^#(s(s(x))) -> c_4(half^#(x))}
==> {half^#(double(x)) -> c_9()}
{half^#(s(s(x))) -> c_4(half^#(x))}
==> {half^#(s(s(x))) -> c_4(half^#(x))}
{half^#(s(s(x))) -> c_4(half^#(x))}
==> {half^#(s(0())) -> c_3()}
{half^#(s(s(x))) -> c_4(half^#(x))}
==> {half^#(0()) -> c_2()}
{-^#(s(x), s(y)) -> c_6(-^#(x, y))}
==> {-^#(s(x), s(y)) -> c_6(-^#(x, y))}
{-^#(s(x), s(y)) -> c_6(-^#(x, y))}
==> {-^#(x, 0()) -> c_5()}
We consider the following path(s):
1) { half^#(s(s(x))) -> c_4(half^#(x))
, half^#(double(x)) -> c_9()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(double(x)) -> c_9()}
Weak Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{half^#(double(x)) -> c_9()}
and weakly orienting the rules
{half^#(s(s(x))) -> c_4(half^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{half^#(double(x)) -> c_9()}
Details:
Interpretation Functions:
double(x1) = [1] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3() = [0]
c_4(x1) = [1] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ half^#(double(x)) -> c_9()
, half^#(s(s(x))) -> c_4(half^#(x))}
Details:
The given problem does not contain any strict rules
2) { half^#(s(s(x))) -> c_4(half^#(x))
, half^#(s(0())) -> c_3()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(s(0())) -> c_3()}
Weak Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{half^#(s(0())) -> c_3()}
and weakly orienting the rules
{half^#(s(s(x))) -> c_4(half^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{half^#(s(0())) -> c_3()}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3() = [0]
c_4(x1) = [1] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ half^#(s(0())) -> c_3()
, half^#(s(s(x))) -> c_4(half^#(x))}
Details:
The given problem does not contain any strict rules
3) { double^#(s(x)) -> c_1(double^#(x))
, double^#(0()) -> c_0()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {double^#(0()) -> c_0()}
Weak Rules: {double^#(s(x)) -> c_1(double^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{double^#(0()) -> c_0()}
and weakly orienting the rules
{double^#(s(x)) -> c_1(double^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{double^#(0()) -> c_0()}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ double^#(0()) -> c_0()
, double^#(s(x)) -> c_1(double^#(x))}
Details:
The given problem does not contain any strict rules
4) { half^#(s(s(x))) -> c_4(half^#(x))
, half^#(0()) -> c_2()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(0()) -> c_2()}
Weak Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{half^#(0()) -> c_2()}
and weakly orienting the rules
{half^#(s(s(x))) -> c_4(half^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{half^#(0()) -> c_2()}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3() = [0]
c_4(x1) = [1] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ half^#(0()) -> c_2()
, half^#(s(s(x))) -> c_4(half^#(x))}
Details:
The given problem does not contain any strict rules
5) { -^#(s(x), s(y)) -> c_6(-^#(x, y))
, -^#(x, 0()) -> c_5()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {-^#(x, 0()) -> c_5()}
Weak Rules: {-^#(s(x), s(y)) -> c_6(-^#(x, y))}
Details:
We apply the weight gap principle, strictly orienting the rules
{-^#(x, 0()) -> c_5()}
and weakly orienting the rules
{-^#(s(x), s(y)) -> c_6(-^#(x, y))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{-^#(x, 0()) -> c_5()}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_5() = [0]
c_6(x1) = [1] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ -^#(x, 0()) -> c_5()
, -^#(s(x), s(y)) -> c_6(-^#(x, y))}
Details:
The given problem does not contain any strict rules
6) {double^#(s(x)) -> c_1(double^#(x))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {double^#(s(x)) -> c_1(double^#(x))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{double^#(s(x)) -> c_1(double^#(x))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{double^#(s(x)) -> c_1(double^#(x))}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [8]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [1] x1 + [1]
c_0() = [0]
c_1(x1) = [1] x1 + [3]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {double^#(s(x)) -> c_1(double^#(x))}
Details:
The given problem does not contain any strict rules
7) {half^#(s(s(x))) -> c_4(half^#(x))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{half^#(s(s(x))) -> c_4(half^#(x))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{half^#(s(s(x))) -> c_4(half^#(x))}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [8]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [1] x1 + [11]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {half^#(s(s(x))) -> c_4(half^#(x))}
Details:
The given problem does not contain any strict rules
8) {-^#(s(x), s(y)) -> c_6(-^#(x, y))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {-^#(s(x), s(y)) -> c_6(-^#(x, y))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{-^#(s(x), s(y)) -> c_6(-^#(x, y))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{-^#(s(x), s(y)) -> c_6(-^#(x, y))}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [8]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_5() = [0]
c_6(x1) = [1] x1 + [11]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {-^#(s(x), s(y)) -> c_6(-^#(x, y))}
Details:
The given problem does not contain any strict rules
9) {if^#(0(), y, z) -> c_7()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {if^#(0(), y, z) -> c_7()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{if^#(0(), y, z) -> c_7()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if^#(0(), y, z) -> c_7()}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {if^#(0(), y, z) -> c_7()}
Details:
The given problem does not contain any strict rules
10)
{if^#(s(x), y, z) -> c_8()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_7() = [0]
c_8() = [0]
c_9() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {if^#(s(x), y, z) -> c_8()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{if^#(s(x), y, z) -> c_8()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{if^#(s(x), y, z) -> c_8()}
Details:
Interpretation Functions:
double(x1) = [0] x1 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
if(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
double^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3() = [0]
c_4(x1) = [0] x1 + [0]
-^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_5() = [0]
c_6(x1) = [0] x1 + [0]
if^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
c_7() = [0]
c_8() = [0]
c_9() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {if^#(s(x), y, z) -> c_8()}
Details:
The given problem does not contain any strict rules